(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_BV)
(declare-fun v0 () (_ BitVec 13))
(declare-fun v1 () (_ BitVec 1))
(declare-fun v2 () (_ BitVec 1))
(declare-fun v3 () (_ BitVec 5))
(declare-fun v4 () (_ BitVec 3))
(assert (let ((e5(_ bv0 1)))
(let ((e6 (bvsub ((_ zero_extend 4) v1) v3)))
(let ((e7 (ite (= ((_ sign_extend 12) v2) v0) (_ bv1 1) (_ bv0 1))))
(let ((e8 ((_ zero_extend 12) e7)))
(let ((e9 (bvadd v3 ((_ sign_extend 4) e5))))
(let ((e10 (bvashr v1 e5)))
(let ((e11 (ite (= e9 ((_ sign_extend 4) e7)) (_ bv1 1) (_ bv0 1))))
(let ((e12 ((_ zero_extend 15) v2)))
(let ((e13 (bvsrem ((_ zero_extend 12) e11) v0)))
(let ((e14 (bvsrem ((_ zero_extend 12) e5) e8)))
(let ((e15 (bvneg e13)))
(let ((e16 (ite (bvule ((_ zero_extend 3) e13) e12) (_ bv1 1) (_ bv0 1))))
(let ((e17 (bvmul ((_ zero_extend 3) e15) e12)))
(let ((e18 (bvnot e16)))
(let ((e19 ((_ repeat 1) e12)))
(let ((e20 ((_ repeat 1) e13)))
(let ((e21 (bvneg e13)))
(let ((e22 (bvneg v4)))
(let ((e23 (bvule v4 ((_ sign_extend 2) e10))))
(let ((e24 (distinct ((_ zero_extend 4) v1) v3)))
(let ((e25 (bvult ((_ zero_extend 12) e7) e13)))
(let ((e26 (distinct e19 ((_ sign_extend 15) e11))))
(let ((e27 (bvult e20 ((_ sign_extend 8) e9))))
(let ((e28 (= ((_ sign_extend 3) e8) e19)))
(let ((e29 (bvsge v4 ((_ sign_extend 2) e11))))
(let ((e30 (bvslt ((_ sign_extend 15) e5) e17)))
(let ((e31 (bvugt e5 v2)))
(let ((e32 (bvsle ((_ zero_extend 12) v2) e8)))
(let ((e33 (= ((_ sign_extend 2) e18) e22)))
(let ((e34 (bvule e21 ((_ zero_extend 12) e11))))
(let ((e35 (distinct ((_ zero_extend 12) e11) e14)))
(let ((e36 (= ((_ sign_extend 3) e20) e17)))
(let ((e37 (bvsle ((_ sign_extend 2) e10) e22)))
(let ((e38 (= ((_ zero_extend 15) e10) e19)))
(let ((e39 (bvuge v3 e9)))
(let ((e40 (bvsgt e12 ((_ zero_extend 3) e20))))
(let ((e41 (bvsge ((_ sign_extend 8) e9) v0)))
(let ((e42 (bvugt e20 e15)))
(let ((e43 (bvslt ((_ sign_extend 2) e18) e22)))
(let ((e44 (distinct ((_ sign_extend 8) e9) e13)))
(let ((e45 (bvsge ((_ sign_extend 4) e16) e6)))
(let ((e46 (=> e36 e40)))
(let ((e47 (not e31)))
(let ((e48 (=> e25 e26)))
(let ((e49 (and e48 e29)))
(let ((e50 (=> e28 e45)))
(let ((e51 (=> e24 e24)))
(let ((e52 (not e46)))
(let ((e53 (and e42 e38)))
(let ((e54 (ite e27 e27 e50)))
(let ((e55 (= e39 e52)))
(let ((e56 (=> e34 e33)))
(let ((e57 (ite e41 e30 e49)))
(let ((e58 (=> e55 e54)))
(let ((e59 (and e51 e58)))
(let ((e60 (xor e23 e32)))
(let ((e61 (xor e35 e35)))
(let ((e62 (=> e43 e47)))
(let ((e63 (not e57)))
(let ((e64 (and e63 e56)))
(let ((e65 (ite e59 e59 e61)))
(let ((e66 (and e37 e65)))
(let ((e67 (and e60 e64)))
(let ((e68 (ite e62 e62 e62)))
(let ((e69 (or e66 e68)))
(let ((e70 (or e67 e53)))
(let ((e71 (=> e44 e69)))
(let ((e72 (or e71 e70)))
(let ((e73 (and e72 (not (= e8 (_ bv0 13))))))
(let ((e74 (and e73 (not (= e8 (bvnot (_ bv0 13)))))))
(let ((e75 (and e74 (not (= v0 (_ bv0 13))))))
(let ((e76 (and e75 (not (= v0 (bvnot (_ bv0 13)))))))
e76
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
